---
title: TLA+ AI Linter
sidebar:
    order: 7
description: Explore how the TLA+ AI Linter leverages GenAI scripts and LLMs to enhance TLA+ specifications with automated linting and consistent comment verification.
keywords: TLA+ linting, AI-powered linter, GenAI integration, automated code review, distributed systems modeling
---
import { Image } from 'astro:assets';
import { Code } from '@astrojs/starlight/components';
import specSource from "../../../../../packages/sample/src/tla/EWD998PCal.tla?raw"
import actionSource from "../../../../../packages/sample/src/tla/PR.yml?raw"
import scriptSource from "../../../../../packages/sample/src/tla/tlAI-Linter.genai.js?raw"
import src from '../../../assets/tla-ai-linter.png';
import alt from "../../../assets/tla-ai-linter.png.txt?raw"


[TLA+](https://lamport.azurewebsites.net/tla/tla.html) is a high-level language for modeling programs and systems--especially
concurrent and distributed ones.  It's based on the idea that the best way to describe things precisely is with simple mathematics.

TLA+ does not come with a traditional linter or formatter.  The TLA+ AI Linter is a GenAI script that uses LLMs to lint TLA+ files.

## TLA+ specifications

The following is a TLA+ spec that models a seminal solution to the [termination detection problem in distributed systems](https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF).

<Code code={specSource} wrap={true} lang="txt" title="EWD998PCal.tla" />

## Script

The following GenAI script will lint the TLA+ spec above.  More specifically, it will check if the prose comments in the spec are consistent with the TLA+ definitions.

<Code code={scriptSource} wrap={true} lang="js" title="tlAI-Linter.genai.mjs" />

- line numbers are added to the file content to help the LLM precisely locate the issues.

```js "lineNumbers" wrap
def("TLA+", env.files.filter(f => f.filename.endsWith(".tla")), {lineNumbers: true})
```

- the script uses a builtin support for [annotations](/genaiscript/reference/scripts/annotations) 
to generate parseable warnings and errors. Annotations are automatically integrated as problems 
in VSCode or as build errors in the CI/CD pipeline.

```js "annotations"
$`Report inconsistent and consistent pairs in a single ANNOTATION section.`
```

- GPT-4 already knows a lot about logic and basic math.  However, the script also lists common TLA+ idioms that are relevant to lint a spec.

## Github Action

<Code code={actionSource} wrap={true} lang="yaml" title="PR.yml" />

- after cloning the repository and installing dependencies such as node.js, the GenAI script is run to lint the TLA+ specs that were added or modified in the PR.

- the script's output, i.e., the annotations generated by the LLM, are formatted as a [SARIF](https://sarifweb.azurewebsites.net) report and [upload](https://docs.github.com/en/code-security/code-scanning/integrating-with-code-scanning/uploading-a-sarif-file-to-github) to the PR.

## Results

The linter generated annotations for each prose comment in the spec, and one comment is found to be inconsistent with the TLA+ definitions.  A corresponding warning is added to the PR.

<Image src={src} alt={alt} />